Inference at * 1 0 1 3 
Iof proof for Lemma integer sqrt:

.....upcase..... NILNIL

1. n : 
2. 0 < n
3. ((n - 1)  0 )  (r:. (((r * r)  (n - 1)) & ((n - 1) < ((r+1) * (r+1)))))
  (n  0 )  (r:. (((r * r)  n) & (n < ((r+1) * (r+1))))) 

latex

 by D 0 

latex

 1: 

 1: 4. n  0 
 1:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
 2: .....wf..... NILNIL

 2:   (n  0 )  
 .

Definitions	x:A  B(x), a < b, A  B, , x:AB(x), i  j , P  Q, x:A. B(x), P & Q, t  T,
Lemmas	le wf, nat wf, ge wf